b:. (b = tt)  (b = ff) 

latex

ProofTree

Definitions	t  T, x:A. B(x), , P  Q, Unit, , , ff, tt
Lemmas	bool wf, bfalse wf, btrue wf